> Maybe I've misunderstood this as a misunderstanding.  The example term 
> representation for the YXML library is exactly the Isabelle term datatype. 
> But that is really just an example, it is not really useful for the 
> problem to connect users to proof checkers.

Oh, I see.

No, it does seem to be the case that Coq's term is much more complicated
than Isabelles.  The analogous datatype for proofterm would be something

    type env = {
      env_globals       : globals;
      env_named_context : named_context;
      env_named_vals    : named_vals;
      env_rel_context   : rel_context;
      env_rel_val       : lazy_val list;
      env_nb_rel        : int;
      env_stratification : stratification;
      retroknowledge : Retroknowledge.retroknowledge }

for the environment.

ProofGeneral-devel mailing list

Reply via email to