]> matita.cs.unibo.it Git - helm.git/commit
- ng_refiner:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Feb 2013 13:47:25 +0000 (13:47 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Feb 2013 13:47:25 +0000 (13:47 +0000)
commitf7da48c844105a52a705872dfa0d4104de010c82
treec150a663dd09baf4cfdd294782a82802594b77cb
parent225887a9f23aac79d4cca907da026917b7df04dc
- ng_refiner:
  now the expected type is `XTNone (was None), `XTSome (was Some, also
  was `Term), `XTSort (any sort, was `Sort), `XTInd (any (co)inductive type).
  `XTProd (was `Prod) is used in "try_coercions"
- we replaced some instances of None with `XTSort or `XTInd through the code.
  lib, lambda, and lambdadelta compile,
  in case of errors like "the term ... is not a sort" or
  "the term ... is not a (co)inductive type", revert to `XTNone in the
  corresponding check.
- Now generated objects have the `Generated attribute properly set
- lambda: many "?" removed because of the improvement in the refiner
          other instances of "?" removed for other reasons
44 files changed:
matita/components/content/notationPp.ml
matita/components/content/notationPt.ml
matita/components/content/notationUtil.ml
matita/components/disambiguation/disambiguate.ml
matita/components/disambiguation/disambiguate.mli
matita/components/disambiguation/disambiguateTypes.ml
matita/components/disambiguation/disambiguateTypes.mli
matita/components/disambiguation/multiPassDisambiguator.mli
matita/components/grafite_engine/grafiteEngine.ml
matita/components/grafite_engine/nCicCoercDeclaration.ml
matita/components/grafite_parser/grafiteParser.ml
matita/components/ng_cic_content/interpretations.ml
matita/components/ng_disambiguation/grafiteDisambiguate.ml
matita/components/ng_disambiguation/grafiteDisambiguate.mli
matita/components/ng_disambiguation/nCicDisambiguate.ml
matita/components/ng_disambiguation/nCicDisambiguate.mli
matita/components/ng_refiner/nCicRefiner.ml
matita/components/ng_refiner/nCicRefiner.mli
matita/components/ng_refiner/nCicUnification.ml
matita/components/ng_refiner/nCicUnification.mli
matita/components/ng_tactics/nCicElim.ml
matita/components/ng_tactics/nDestructTac.ml
matita/components/ng_tactics/nInversion.ml
matita/components/ng_tactics/nTacStatus.ml
matita/components/ng_tactics/nTacStatus.mli
matita/components/ng_tactics/nTactics.ml
matita/components/ng_tactics/nnAuto.ml
matita/matita/contribs/lambda/background/preamble.ma
matita/matita/contribs/lambda/paths/dst_computation.ma
matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma
matita/matita/contribs/lambda/paths/labeled_st_computation.ma
matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
matita/matita/contribs/lambda/paths/path.ma
matita/matita/contribs/lambda/paths/standard_order.ma
matita/matita/contribs/lambda/paths/standard_trace.ma
matita/matita/contribs/lambda/paths/trace.ma
matita/matita/contribs/lambda/subterms/relocating_substitution.ma
matita/matita/contribs/lambda/subterms/relocation.ma
matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma
matita/matita/contribs/lambda/terms/parallel_reduction.ma
matita/matita/contribs/lambda/terms/relocating_substitution.ma
matita/matita/contribs/lambda/terms/relocation.ma
matita/matita/contribs/lambda/terms/sequential_computation.ma
matita/matita/matitaScript.ml